(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 4))
(declare-fun v1 () (_ BitVec 10))
(declare-fun v2 () (_ BitVec 8))
(declare-fun v3 () (_ BitVec 12))
(declare-fun v4 () (_ BitVec 12))
(declare-fun a5 () (Array  (_ BitVec 11)  (_ BitVec 3)))
(declare-fun a6 () (Array  (_ BitVec 12)  (_ BitVec 1)))
(declare-fun a7 () (Array  (_ BitVec 5)  (_ BitVec 8)))
(assert (let ((e8(_ bv4043 12)))
(let ((e9(_ bv0 1)))
(let ((e10 (bvor ((_ sign_extend 11) e9) v4)))
(let ((e11 (bvashr ((_ zero_extend 4) v0) v2)))
(let ((e12 (bvsdiv ((_ sign_extend 4) v2) e8)))
(let ((e13 (bvand v3 v4)))
(let ((e14 (ite (bvsgt v1 v1) (_ bv1 1) (_ bv0 1))))
(let ((e15 (store a6 e8 ((_ extract 3 3) v0))))
(let ((e16 (store a5 ((_ zero_extend 7) v0) ((_ extract 7 5) e12))))
(let ((e17 (select a5 ((_ extract 10 0) e12))))
(let ((e18 (select e16 ((_ extract 11 1) e13))))
(let ((e19 (store e15 ((_ sign_extend 4) e11) ((_ extract 4 4) e13))))
(let ((e20 (select e19 ((_ zero_extend 11) e14))))
(let ((e21 (ite (bvslt ((_ zero_extend 9) e17) e8) (_ bv1 1) (_ bv0 1))))
(let ((e22 (bvsdiv ((_ sign_extend 8) v0) e10)))
(let ((e23 (ite (bvslt v3 e12) (_ bv1 1) (_ bv0 1))))
(let ((e24 (bvlshr e10 v3)))
(let ((e25 (bvxor e13 e13)))
(let ((e26 (ite (distinct v4 ((_ zero_extend 11) e20)) (_ bv1 1) (_ bv0 1))))
(let ((e27 ((_ sign_extend 2) v2)))
(let ((e28 (ite (= (_ bv1 1) ((_ extract 6 6) e11)) e17 ((_ zero_extend 2) e9))))
(let ((e29 (bvmul e14 e14)))
(let ((e30 (ite (bvule ((_ sign_extend 2) v1) v4) (_ bv1 1) (_ bv0 1))))
(let ((e31 (ite (distinct ((_ sign_extend 9) e18) v3) (_ bv1 1) (_ bv0 1))))
(let ((e32 (bvslt ((_ sign_extend 5) e18) v2)))
(let ((e33 (= e24 e25)))
(let ((e34 (bvsgt ((_ zero_extend 5) e18) e11)))
(let ((e35 (distinct e10 e25)))
(let ((e36 (bvsgt e21 e23)))
(let ((e37 (bvsle e25 ((_ sign_extend 11) e26))))
(let ((e38 (bvsle e17 ((_ sign_extend 2) e31))))
(let ((e39 (bvuge e24 ((_ zero_extend 2) e27))))
(let ((e40 (bvugt e25 e8)))
(let ((e41 (bvuge e8 ((_ sign_extend 11) e23))))
(let ((e42 (distinct e22 e22)))
(let ((e43 (bvslt ((_ zero_extend 1) e17) v0)))
(let ((e44 (= e12 e13)))
(let ((e45 (bvslt e24 ((_ sign_extend 9) e18))))
(let ((e46 (bvugt e8 ((_ sign_extend 11) e29))))
(let ((e47 (bvsle e31 e9)))
(let ((e48 (bvugt e22 ((_ zero_extend 11) e29))))
(let ((e49 (bvsgt e8 ((_ zero_extend 9) e28))))
(let ((e50 (bvsle v1 e27)))
(let ((e51 (bvsge ((_ sign_extend 11) e9) e25)))
(let ((e52 (bvsgt ((_ sign_extend 9) e14) e27)))
(let ((e53 (bvslt ((_ sign_extend 9) e18) e22)))
(let ((e54 (bvult v2 ((_ zero_extend 7) e30))))
(let ((e55 (bvugt e8 e25)))
(let ((e56 (bvsle ((_ sign_extend 8) v0) e8)))
(let ((e57 (bvslt e31 e9)))
(let ((e58 (bvugt ((_ sign_extend 9) e17) e13)))
(let ((e59 (bvsge e23 e29)))
(let ((e60 (bvslt e23 e21)))
(let ((e61 (bvult e13 ((_ zero_extend 11) e30))))
(let ((e62 (bvuge v4 ((_ zero_extend 11) e9))))
(let ((e63 (bvuge e12 ((_ zero_extend 11) e26))))
(let ((e64 (bvult ((_ zero_extend 7) e29) v2)))
(let ((e65 (= e12 ((_ sign_extend 8) v0))))
(let ((e66 (bvslt ((_ zero_extend 2) e23) e28)))
(let ((e67 (bvslt e21 e14)))
(let ((e68 (distinct e29 e9)))
(let ((e69 (bvule e12 ((_ sign_extend 9) e18))))
(let ((e70 (bvsge e29 e31)))
(let ((e71 (= v2 ((_ sign_extend 7) e23))))
(let ((e72 (bvsge e17 e28)))
(let ((e73 (distinct e10 ((_ sign_extend 8) v0))))
(let ((e74 (distinct e10 ((_ sign_extend 9) e28))))
(let ((e75 (bvuge e25 ((_ zero_extend 4) v2))))
(let ((e76 (bvugt ((_ sign_extend 2) v1) e24)))
(let ((e77 (= ((_ sign_extend 9) e28) e10)))
(let ((e78 (bvuge e29 e14)))
(let ((e79 (bvsgt ((_ sign_extend 11) e20) e8)))
(let ((e80 (bvule e22 ((_ zero_extend 11) e26))))
(let ((e81 (bvslt ((_ zero_extend 11) e30) e25)))
(let ((e82 (= e29 e30)))
(let ((e83 (= ((_ sign_extend 11) e26) v3)))
(let ((e84 (= e76 e63)))
(let ((e85 (= e35 e34)))
(let ((e86 (ite e60 e71 e45)))
(let ((e87 (not e56)))
(let ((e88 (= e70 e42)))
(let ((e89 (ite e68 e83 e50)))
(let ((e90 (= e54 e61)))
(let ((e91 (or e39 e72)))
(let ((e92 (= e48 e52)))
(let ((e93 (=> e43 e84)))
(let ((e94 (ite e86 e33 e66)))
(let ((e95 (ite e47 e90 e94)))
(let ((e96 (and e91 e85)))
(let ((e97 (and e82 e75)))
(let ((e98 (= e49 e41)))
(let ((e99 (= e93 e80)))
(let ((e100 (not e65)))
(let ((e101 (not e96)))
(let ((e102 (=> e55 e32)))
(let ((e103 (ite e78 e53 e78)))
(let ((e104 (= e77 e102)))
(let ((e105 (and e97 e64)))
(let ((e106 (xor e104 e101)))
(let ((e107 (xor e62 e87)))
(let ((e108 (or e38 e103)))
(let ((e109 (not e69)))
(let ((e110 (= e57 e105)))
(let ((e111 (not e58)))
(let ((e112 (or e74 e73)))
(let ((e113 (xor e107 e67)))
(let ((e114 (xor e99 e110)))
(let ((e115 (=> e92 e109)))
(let ((e116 (not e100)))
(let ((e117 (=> e116 e81)))
(let ((e118 (not e106)))
(let ((e119 (and e89 e44)))
(let ((e120 (= e118 e95)))
(let ((e121 (not e51)))
(let ((e122 (and e114 e79)))
(let ((e123 (or e40 e113)))
(let ((e124 (xor e123 e98)))
(let ((e125 (= e121 e112)))
(let ((e126 (or e46 e117)))
(let ((e127 (xor e119 e37)))
(let ((e128 (ite e111 e127 e108)))
(let ((e129 (or e122 e126)))
(let ((e130 (and e59 e115)))
(let ((e131 (or e36 e36)))
(let ((e132 (=> e128 e131)))
(let ((e133 (not e88)))
(let ((e134 (= e124 e133)))
(let ((e135 (xor e125 e129)))
(let ((e136 (xor e120 e134)))
(let ((e137 (ite e136 e130 e130)))
(let ((e138 (not e135)))
(let ((e139 (= e137 e137)))
(let ((e140 (and e132 e138)))
(let ((e141 (= e139 e140)))
(let ((e142 (and e141 (not (= e10 (_ bv0 12))))))
(let ((e143 (and e142 (not (= e10 (bvnot (_ bv0 12)))))))
(let ((e144 (and e143 (not (= e8 (_ bv0 12))))))
(let ((e145 (and e144 (not (= e8 (bvnot (_ bv0 12)))))))
e145
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
